Nuprl Lemma : null-seq_wf
11,40
postcript
pdf
T
:Type. null
{0..0
}
T
latex
Definitions
Type
,
t
T
,
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
,
{
x
:
A
|
B
(
x
)}
,
{
i
..
j
}
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Unit
,
,
#$n
,
x
.
A
(
x
)
,
null
Lemmas
int
seg
wf
,
it
wf
origin
T:Type. null 
{0..0
}
T T:Type. null {0..0}T T
Q
A
B j < k
}B(x)x:A. B(x)
x.A(x)